feat: add Alternative.{many,many1} #1595
Conversation
github-actions
bot
added
the
awaiting-review
|
Please add a copyright header and follow style from similar files. |
fgdorais
added
awaiting-author
fgdorais
changed the title
414owen
force-pushed
the
os/alternative-many
branch
from
7fc04f7 to
65ab39c
Compare
|
I made a few minor edits, mostly so that CI works. I hope you don't mind, it was easier to do than to explain. PS: Avoid force push. |
Absolutely fine. Be my guest. |
|
Mathlib CI status (docs):
|
| def many1 [Alternative f] | ||
| (p : f α) : f (Σ n, Vector α (1 + n)) := | ||
| let g x xs := ⟨xs.1, Vector.singleton x ++ xs.2⟩ | ||
| let toVec (l : List α) : Σ n, Vector α n := | ||
| let arr := List.toArray l | ||
| ⟨arr.size, ⟨arr, rfl⟩⟩ | ||
| let manyVec : f (Σ n, (Vector α n)) := toVec <$> Alternative.many p | ||
| g <$> p <*> manyVec <|> Alternative.failure |
There was a problem hiding this comment.
Happy to wait for pending Zulip discussion; but the two many1 functions in Lean already are the much simpler
| def many1 [Alternative f] | |
| (p : f α) : f (Σ n, Vector α (1 + n)) := | |
| let g x xs := ⟨xs.1, Vector.singleton x ++ xs.2⟩ | |
| let toVec (l : List α) : Σ n, Vector α n := | |
| let arr := List.toArray l | |
| ⟨arr.size, ⟨arr, rfl⟩⟩ | |
| let manyVec : f (Σ n, (Vector α n)) := toVec <$> Alternative.many p | |
| g <$> p <*> manyVec <|> Alternative.failure | |
| def many1 [Alternative f] (p : f α) : f (List α) := | |
| List.cons <$> p <*> many p |
in the absence of a concrete use case requiring the complexity, I'd be inclined to pick this much simpler option.
There was a problem hiding this comment.
(note that independently, the <|> Alternative.failure looks like a no-op to me)
There was a problem hiding this comment.
def many1 [Alternative f] (p : f α) : f (List α) :=
List.cons <$> p <*> many p
I'm not a huge fan of this version to be honest. It means that, even though you know there's at least one element, operations like head, and tail are partial.
It throws away useful information, and goes against "make error states unrepresentable" / "parse, don't validate", etc.
There was a problem hiding this comment.
True, but my proposal is consistent with Std.Internal.Parsec.many1 from the standard library.
There was a problem hiding this comment.
That is something I can't deny :)
The design for `many1` doesn't seem very clear-cut, it's sparked quite a bit of discourse in zulip: https://leanprover.zulipchat.com/#narrow/channel/348111-batteries/topic/Nonempty.20List.20Type/with/567406954 Let's defer it to another PR.
|
Since |
414owen
changed the title
|
Please bring back |
This reverts commit d5d7e84.
414owen
changed the title
|
Please edit the |
|
I've rebased this PR on |
|
You should no longer need Using PS: I will soon be away for the next few days. Don't worry, I'll be back next week at the latest. |
Are you sure about that? Could be written monadically, for clarity: So the first thing parsed should end up as the head of the list, unless I'm missing something? |
|
I think you're right! This needs some tests to ensure this is the actual behavior. |
leanprover-community-mathlib4-bot
added
the
merge-conflict
5 participants
Closes #1577